\begin{tabbing}
FIFO\=\{i:l\}\+
\\[0ex](${\it es}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$C$:Type\{i\}\+
\\[0ex]$\times$ ($T$:Type\{i\}
\\[0ex]$\times$ $S$:($C$$\rightarrow$$C$$\rightarrow$es{-}E(${\it es}$)$\rightarrow\mathbb{P}$\{i\})
\\[0ex]$\times$ $R$:($C$$\rightarrow$es{-}E(${\it es}$)$\rightarrow\mathbb{P}$\{i\})
\\[0ex]$\times$ ${\it codes}$:($j$:$C$$\rightarrow$$i$:$C$$\rightarrow$$e$:\{$x$:es{-}E(${\it es}$)$\mid$ $S$($j$,$i$,$x$)\} $\rightarrow$es{-}state(${\it es}$;es{-}loc(${\it es}$; $e$))$\rightarrow$$T$)
\\[0ex]$\times$ (${\it decodes}$:($i$:$C$$\rightarrow$$e$:\{$x$:es{-}E(${\it es}$)$\mid$ $R$($i$,$x$)\} $\rightarrow$es{-}state(${\it es}$;es{-}loc(${\it es}$; $e$))$\rightarrow$$T$)
\\[0ex]$\times$ fifo(${\it es}$;${\it codes}$;${\it decodes}$;$C$;$S$;$R$;$T$)))
\-
\end{tabbing}